L1,L2. 
i:
(||L1||-1). P(L1,i) & L2 = swap(L1;i;i+1))^*
clarification:
guarded_permutation(T;P)
== rel_star(T List;(
L1,L2. i:{0..(||L1||-1)
}. P(L1,i) & L2 = swap(L1;i;i+1) 
T List)) | 4,23 |
L1,L2. i:(||L1||-1). P(L1,i) & L2 = swap(L1;i;i+1))^*
L1,L2. i:{0..(||L1||-1)}. P(L1,i) & L2 = swap(L1;i;i+1) T List))
| Definitions | x:A. B(x)} |
| FDL editor aliases | guarded_permutation |